Termination w.r.t. Q of the following Term Rewriting System could be disproven:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

Q is empty.


↳ QTRS
  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)


Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(g(X), Y))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(g(X), Y))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(g(X), Y)) at position [1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(g(X), Y)))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(g(X), Y)))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(g(X), Y))) at position [1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(g(X), Y))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(g(X), Y))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(g(X), Y)))) at position [1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(g(X), Y)))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(g(X), Y)))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(g(X), Y))))) at position [1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))) at position [1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))) at position [1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))) at position [1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))
F(g(X), Y) → F(g(X), Y)

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))) at position [1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))) at position [1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))) at position [1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))
F(g(X), Y) → F(g(X), Y)

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))
F(g(X), Y) → F(g(X), Y)

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))
F(g(X), Y) → F(g(X), Y)

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))))))
F(g(X), Y) → F(g(X), Y)

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y)))))))))))))))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))))))) at position [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] we obtained the following new rules:

F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))))))))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)
F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))))))))

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


F(g(X), Y) → F(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(X, f(g(X), Y))))))))))))))))))))))))))))))))))))))))))))))))))))
The remaining pairs can at least be oriented weakly.

F(g(X), Y) → F(g(X), Y)
Used ordering: Polynomial interpretation with max and min functions [25]:

POL(F(x1, x2)) = x1   
POL(f(x1, x2)) = 0   
POL(g(x1)) = 1 + x1   

The following usable rules [17] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                                  ↳ QDPOrderProof
                                                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                                                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)

The TRS R consists of the following rules:

f(g(X), Y) → f(X, f(g(X), Y))

The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                                  ↳ QDPOrderProof
                                                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                                                      ↳ UsableRulesProof
                                                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                                                          ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)

R is empty.
The set Q consists of the following terms:

f(g(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

f(g(x0), x1)



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Rewriting
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ Rewriting
                        ↳ QDP
                          ↳ Rewriting
                            ↳ QDP
                              ↳ Rewriting
                                ↳ QDP
                                  ↳ Rewriting
                                    ↳ QDP
                                      ↳ Rewriting
                                        ↳ QDP
                                          ↳ Rewriting
                                            ↳ QDP
                                              ↳ Rewriting
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ Rewriting
                                                            ↳ QDP
                                                              ↳ Rewriting
                                                                ↳ QDP
                                                                  ↳ Rewriting
                                                                    ↳ QDP
                                                                      ↳ Rewriting
                                                                        ↳ QDP
                                                                          ↳ Rewriting
                                                                            ↳ QDP
                                                                              ↳ Rewriting
                                                                                ↳ QDP
                                                                                  ↳ Rewriting
                                                                                    ↳ QDP
                                                                                      ↳ Rewriting
                                                                                        ↳ QDP
                                                                                          ↳ Rewriting
                                                                                            ↳ QDP
                                                                                              ↳ Rewriting
                                                                                                ↳ QDP
                                                                                                  ↳ Rewriting
                                                                                                    ↳ QDP
                                                                                                      ↳ Rewriting
                                                                                                        ↳ QDP
                                                                                                          ↳ Rewriting
                                                                                                            ↳ QDP
                                                                                                              ↳ Rewriting
                                                                                                                ↳ QDP
                                                                                                                  ↳ Rewriting
                                                                                                                    ↳ QDP
                                                                                                                      ↳ Rewriting
                                                                                                                        ↳ QDP
                                                                                                                          ↳ Rewriting
                                                                                                                            ↳ QDP
                                                                                                                              ↳ Rewriting
                                                                                                                                ↳ QDP
                                                                                                                                  ↳ Rewriting
                                                                                                                                    ↳ QDP
                                                                                                                                      ↳ Rewriting
                                                                                                                                        ↳ QDP
                                                                                                                                          ↳ Rewriting
                                                                                                                                            ↳ QDP
                                                                                                                                              ↳ Rewriting
                                                                                                                                                ↳ QDP
                                                                                                                                                  ↳ Rewriting
                                                                                                                                                    ↳ QDP
                                                                                                                                                      ↳ Rewriting
                                                                                                                                                        ↳ QDP
                                                                                                                                                          ↳ Rewriting
                                                                                                                                                            ↳ QDP
                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                ↳ QDP
                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                    ↳ QDP
                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                        ↳ QDP
                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                            ↳ QDP
                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                  ↳ Rewriting
                                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                                      ↳ Rewriting
                                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                                          ↳ Rewriting
                                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                                              ↳ Rewriting
                                                                                                                                                                                                                ↳ QDP
                                                                                                                                                                                                                  ↳ QDPOrderProof
                                                                                                                                                                                                                    ↳ QDP
                                                                                                                                                                                                                      ↳ UsableRulesProof
                                                                                                                                                                                                                        ↳ QDP
                                                                                                                                                                                                                          ↳ QReductionProof
                                                                                                                                                                                                                            ↳ QDP
                                                                                                                                                                                                                              ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

F(g(X), Y) → F(g(X), Y)

The TRS R consists of the following rules:none


s = F(g(X), Y) evaluates to t =F(g(X), Y)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from F(g(X), Y) to F(g(X), Y).